| Definitions |  x:A. B(x), P   Q, P & Q, t  T,  ,   x. t(x),  b, t.1, triggersGlue(A; l; tg; ds; conds), t.2, es-realizer(p), sframe-p-realizable,  (L), if b then t else f fi , reduce(f;k;as), Y, True, Rplus?(x1), ff, tt, Rplus-left(x1), Rplus-right(x1), Knd, State(ds), Normal(T), conditional-send-p-realizable, es-real-monotonicity, sends-p-realizable, DeclaredType(ds;x), S  T, Top, sender-glues-triggers-p(es; A; l; tg; ds; conds), es-triggers-params-consistent(es;A;i;ds;conds),  x:A. B(x), state@i, x(s), P  Q, P Q, Realizer,  es.P(es), R ||- es.P(es), {T}, False, Unit, (x l), f(x), isrcv(k),  , isrcvl(l;k), can-apply(f;x), p   q, isl(x), only events in L send on l with tg, k(v:B) sends on l [tg:T, f <state, v>]?[], A c B, Rsframe(lnk;tag;L), Rsends(ds;knd;T;l;dt;g), left right, Rnone(),  , Rinit(loc;T;x;v), Rframe(loc;T;x;L), Reffect(loc;ds;knd;T;x;f), Rpre(loc;ds;a;p;P), Raframe(loc;k;L), Rbframe(loc;k;L), Rrframe(loc;x;L), fpf-domain(f) |
| Lemmas | triggersGlue wf, triggersGlue feasible, implies-es-real, sender-glues-triggers-p wf, event system wf, R-consistent wf, Knd wf, l member wf, fpf-domain wf, fpf-trivial-subtype-top, decl-state wf, top wf, pi1 wf, fpf-ap wf, Kind-deq wf, member-fpf-domain, not wf, rcv wf, normal-type wf, normal-ds wf, assert wf, fpf-dom wf, hasloc wf, lsrc wf, fpf wf, Id wf, IdLnk wf, es-real wf, sframe-p wf, R-sub-implies, true wf, false wf, es realizer wf, unit wf, rationals wf, decl-type wf, finite-prob-space wf, bool wf, R-sub-plus-left, isrcv wf, ldst wf, lnk wf, conditional-send-p wf, member-fpf-dom, pi2 wf, fpf-cap wf, id-deq wf, R-sub-Rall2, Rsends wf, isrcvl wf, eqtt to assert, fpf-join wf, fpf-single wf, tagof wf, assert-isrcvl, iff transitivity, bnot wf, eqff to assert, assert of bnot, fpf-single wf3, can-apply wf, do-apply wf, R-sub-plus-right3, assert-hasloc, fpf-cap-single-join, fpf-cap-single1, sender-frame-glues-triggers, es-kind wf, es-sender wf, es-kind-rcv, es-loc wf, es-state-subtype, es-vartype wf |
Type, conds:k:Knd fp
(State(ds)
(k = rcv(l,tg)))))